| Definitions | x:A  B(x), P  Q, es-locl(es; e; e'), x f y,  x:A. B(x), x:A  B(x), P   Q, P  Q, idlnk-deq, es-eq(es), rcv-from-on(dE; dL; info; e; l; r),  x.A(x), eventlist(pred?; e), receives(dE; dL; pred?; info; p; e; l), es-receives(es; e; l), EOrderAxioms(E;pred?;info), prop{i:l}, IdLnk, e < e', left + right,  x:A. B(x), P  Q, sender(e), rcv?(e), Type, a < b,  , {x:A| B(x)} , f(a), l_before(x; y; l; T), l-ordered(T; x,y.R(x;y); L), loc-ordered(es; L), event_system{i:l}, es-pred?(es), es_info(es), Id, es-E(es), es-oaxioms(es), t.1, sends-bound(p; e; l), t  T, pred(e), s = t, first(e),  b,  A, A c B, SWellFounded(R(x;y)), pred!(e;e'), es-causl(es; e; e'), void, rel_implies(T; R1; R2), False |